$\forall$$M_{1}$, $M_{2}$:MsgA. \\[0ex]$M_{1}$ $\subseteq$ $M_{2}$ $\Rightarrow$ ($\forall$$k$:Knd, $l$:IdLnk. $M_{2}$.bframe($k$ sends on $l$) $\Rightarrow$ $M_{1}$.bframe($k$ sends on $l$))